COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	more arithmetic
C00005 00003	minus
C00007 00004	proofs of facts about arithmetic
C00011 00005	minus
C00017 ENDMK
C⊗;
;more arithmetic
(wipe-out)
(get-proofs normal prf ekl sys)
(get-proofs natnum prf ekl sys)
(label simpinfo zero_not_successor) ;add these to simpinfo for now
(label simpinfo zeroleast1)
(label simpinfo successorless)
(label simpinfo successoreq)
(label simpinfo zeroleast3)

(proof lesseq)


;1
(axiom |∀n.¬n=n'|)
(label simpinfo)

;2
(decl lesseq (type: |ground⊗ground→truthval|)
      (infixname: |≤|)(bindingpower: 920))

;3 
(define lesseq |∀m n.(m ≤ n)=(m=n∨m<n)|)
(label lesseqdef)

;4
(axiom |∀n m.n'≤m'≡n≤m|)
(label successorlesseq) (label successorfacts) (label simpinfo)

;5
(axiom |∀n m k.n≤m∧m≤k⊃n≤k|)
(label trans_lesseq)

;6
(axiom |∀n m k.n<m∧m≤k⊃n<k|)
(label less_lesseq_fact1)

;7
(axiom |∀n.0≤n|)
(label zeroleast)

;8
(axiom |∀n.1≤n'|)
(label oneleastsucc)

;9
(axiom |∀n m.n'<m⊃¬m=0|)
(label zero_non_less_successor)(label simpinfo)

;10
(axiom |∀m n.m'<n⊃m<n|)
(label succ_less_less)

;11
(axiom |∀m n.m'≤n⊃m≤n|)
(label succ_lesseq_lesseq)

;12
(axiom |∀n m.n≤m⊃n≤m'|)
(label lesseq_lesseq_succ)

;13
(axiom |∀n m.m<n'≡m≤n|)
(label less_succ_lesseq)

;14
(axiom |∀m n.m<n=m'≤n|)
(label less_lesseqsucc)

;15
(axiom |∀n m.n≤m∧m≤n⊃n=m|)
(label leq_leq_eq)

;16
(axiom |∀n m.m<n∨m=n∨n<m|)
(label trichotomy)

;minus
(proof minus)
;1. 
(decl minus (type: |ground⊗ground→ground|)(infixname: |-|)(bindingpower: 940))

;2. 
(define minus |∀m n.m-0=m∧m-(n')=pred(m-n)| inductive_definition)
(label minusdef)

;3.
(axiom |∀n k.natnum(k-n)|)
(label simpinfo)(label minus_sort)

;4.
(axiom |∀n m.n<m⊃0<m-n|)
(label minusfact3)

;5.
(axiom |∀n.0<n⊃pred(n)'=n|)
(label minusfact5)

;6.
(axiom |∀n m.n≤m⊃m'-n=(m-n)'|)
(label successor_minus)

;7.
(axiom |∀n m.n<m⊃m-n=(m-(n'))'|)
(label minusfact10)

;8.
(axiom |∀n m.m<n⊃n-(m')<n|)
(label minusfact11)

;9.
(axiom |∀n.n-n=0|)
(label simpinfo)(label n_less_n)

;10.
(axiom |∀n.0<n⊃n-(pred n)=1|)
(label minus1)

;11.
(axiom |∀n m.m≤n⊃m-n=0|)
(label total_subtraction)

;12.
(axiom |∀n m k.k<n∧m<n-k≡m+k<n|)
(label inequality_law)

;the main facts of arithmetic needed for the pigeon-hole

;13.
(axiom |∀n k m.n≤m∧1≤k⊃n'≤m+k|)
(label add_lesseq)

;14.
(axiom |∀k n m.1≤k∧m+k=n'∧n≤m⊃1=k∧n=m|)
(label add_one)
(save-proofs minus)
;proofs of facts about arithmetic
(wipe-out)
(get-proofs minus prf ekl sys)
(proof lesseq)

;1
(unlabel simpinfo lesseq#1)

(ue (a |λn.¬n=n'|) proof_by_induction)

(label simpinfo lesseq#1)

;4
;successorlesseq
(unlabel simpinfo successorlesseq)

(trw  |∀n m.n'≤m'≡n≤m| (open lesseq))

(label simpinfo successorlesseq)

;5
;trans_lesseq

(trw |∀n m k.n≤m∧m≤k⊃n≤k| (open lesseq)
     (use normal mode: always) transitivity_of_order)
;∀N M K.N≤M∧M≤K⊃N≤K

;6
;less_lesseq_fact1

(trw |∀n m k.n<m∧m≤k⊃n<k| (open lesseq)
     (use normal mode: always) transitivity_of_order)
;∀N M K.N<M∧M≤K⊃N<K

;7
;zeroleast

(ue (a |λn.0≤n|) proof_by_induction 
    (part 1 (open lesseq)))
;∀N.0≤N

;8
;oneleastsucc

(trw |0'≤n'| zeroleast)
;0'≤N'

(rw * (nuse successorlesseq))
;1≤N'

;9
;zero non less successor
(unlabel simpinfo  zero_non_less_successor)

(trw |m=0∧n'<m|)
(derive |n'<m⊃¬m=0| *)

(label simpinfo  zero_non_less_successor)

;a couple of very trivial facts
;10
;succ_less_less

(trw |∀m n.m'<n⊃m<n| transitivity_of_order successor1)

;11
;succ_lesseq_lesseq

(derive |M'=N⊃M<N| successor1)

(trw |∀m n.m'≤n⊃m≤n|(open lesseq) 
   succ_less_less * (use normal mode: always))
;∀M N.M'≤N⊃M≤N

;12
;lesseq_lesseq_succ
(trw |∀n m.n≤m⊃n≤m'| (open lesseq)(use normal mode: always) 
        (successor1 transitivity_of_order))

;13
;"m less succ of n" implies "m lesseq n"
(ue (a |λn.n<0'≡n≤0|) proof_by_induction (part 1(open lesseq)))
;∀N.N<1≡N≤0

(ue (a2 |λn m.m<n'≡m≤n|) proof_by_doubleinduction * zeroleast)
;∀N M.M<N'≡M≤N

;14
;"n less than m" implies "succ of n lesseq m"

(ue (a |λn.0<n≡0'≤n|) proof_by_induction 
    zeroleast (part 1#1 (open lesseq)))
;∀N.0<N≡1≤N

(ue (a2 |λn m.n<m≡n'≤m|) proof_by_doubleinduction 
    * (part 1#1#2(open lesseq)))
;∀N M.N<M≡N'≤M

;15
;"n lesseq m" and "m lesseq n" implies "n equal m"

(ue (a2 |λn m.n≤m∧m≤n⊃n=m|) proof_by_doubleinduction 
        (part 1 (open lesseq) (use normal mode: always)) )

;16
;trichotomy
(rw zeroleast (open lesseq))

(ue (a2 |λn m.m<n∨m=n∨n<m|) proof_by_doubleinduction (use normal mode: always) *)
;∀N M.M<N∨M=N∨N<M

;minus
(wipe-out)
(get-proofs minus prf ekl sys)
(proof minus)

;3.
(unlabel simpinfo minus_sort)
;the following proof works because pred is a total function

(ue (a |λn.∀k.natnum(k-n)|) proof_by_induction (part 1(open minus)))
;∀N K.NATNUM(K-N)

(label simpinfo minus_sort)

;4.
;minusfact3

(ue (a |λn.n<m'⊃pred(m'-n)=m-n|) proof_by_induction (part 1(open minus pred))
         succ_less_less)
;∀N.N<M'⊃PRED(M'-N)=M-N

(ue (a2 |λn m.n<m⊃0<m-n|) proof_by_doubleinduction (open minus) 
        (use * mode: always) succ_less_less)
;∀N M.N<M⊃0<M-N

;5.
;minusfact5

(ue (a |λn.0<n⊃pred(n)'=n|) proof_by_induction)
;∀N.0<N⊃PRED(N)'=N

;6.
;successor minus

(ue (a |λn.n<m'⊃m'-n=(m-n)'|) proof_by_induction 
  (use -2 -3  successor1 succ_less_less mode: exact)
    (use * ue: ((n.|m-n|)) )(part 1(open minus pred)))
;∀N.N<M'⊃M'-N=(M-N)'

(derive |∀n m.n≤m⊃m'-n=(m-n)'| (* less_succ_lesseq))


(trw |∀n m.n≤m⊃pred(m'-n)=m-n| successor_minus)
;∀N M.N≤M⊃PRED(M'-N)=M-N
(label minusfact7)

;7.
;minusfact10
(trw |∀n m.n<m⊃(m-n')'=m-n| (use minusfact5 ue: ((n.|m-n|)) ) minusfact3 (open minus))
;∀N M.N<M⊃(M-N')'=M-N

;8.
;minusfact11
(rw successor_minus (open lesseq)(use normal mode: always))
(derive |∀N M.N<M⊃M'-N=(M-N)'| *)

(ue (a |λn.0<n⊃pred(n)<n|) proof_by_induction successor1)
;∀N.0<N⊃PRED(N)<N

(ue (a2 |λn m.m<n⊃n-(m')<n|) proof_by_doubleinduction 
 (part 1(use * -2 minusdef mode: always))(transitivity_of_order successor1))
;∀N M.M<N⊃N-M'<N

;9.
;n less n
(unlabel simpinfo n_less_n)

(rw successor_minus (open lesseq)(use normal mode: always))
(derive |∀N M.N=M⊃M'-N=(M-N)'| *)
(ue (a |λn.n-n=0|) proof_by_induction 
    (part 1(use * mode: always)(open minus)))
;∀N.N-N=0

(label simpinfo n_less_n)

;10.
;minus1

(ue ((n.n)(m.|n|)) successor_minus (open lesseq))
(ue (a |λn.0<n⊃n-(pred n)=1|) proof_by_induction  (open pred) *
      (use successor_minus n_less_n mode: exact))

;11.
;total subtraction
(ue (a |λn.m<n⊃m-n=0|) proof_by_induction (open minus lesseq)  
   (use less_succ_lesseq mode: exact) (use normal mode: always))
;∀N.M<N⊃M-N=0

(trw |∀N M.M≤N⊃M-N=0| (open lesseq) (use normal mode: always) * n_less_n)
;∀N M.M≤N⊃M-N=0

;12.
(derive |∀k n.k<n'⊃n'-k=(n-k)'| (successor_minus less_succ_lesseq))
(ue (a2 |λn m.n<m⊃0<m-n|) proof_by_doubleinduction (open minus) 
   (use * mode: always)(use succ_less_less))
;∀N M.N<M⊃0<M-N

(ue (a2 |λn m.k<n∧m<n-k≡m+k<n|) proof_by_doubleinduction (use * -2 mode: always))
;(∀N M.K<N∧M<N-K≡M+K<N⊃K<N'∧M<N-K≡M+K<N)⊃(∀N M.K<N∧M<N-K≡M+K<N)

(rw * (use less_succ_lesseq mode: exact) (open lesseq)(use normal mode: always))
;∀N M.K<N∧M<N-K≡M+K<N

;13.
;add_lesseq

(trw |∀n.0'≤n'| (use zeroleast))
(rw * (nuse successorlesseq))
;∀N.1≤N'

(ue (a |λn.0≤n∧1≤k⊃1≤n+k|) proof_by_induction *)
;∀N.0≤N∧1≤K⊃1≤N+K

(trw |∀n.n≤0⊃n=0| (open lesseq))
;∀N.N≤0⊃N=0

(ue (a2 |λn m.n≤m∧1≤k⊃n'≤m+k|) proof_by_doubleinduction 
        -2 (use * mode: always))
;∀N M.N≤M∧1≤K⊃N'≤M+K

;14.
;add_one

(ue (a2 |λm k.0'≤k∧0'=m+k⊃1=k∧0=m|) proof_by_doubleinduction 
        (part 1 (open lesseq)(use normal mode: always)))
;∀N M.1≤M∧1=N+M⊃1=M∧0=N

(ue (a2 |λn m.1≤k∧n'=m+k∧n≤m⊃1=k∧n=m|) proof_by_doubleinduction 
        (part 1#1#2 (open lesseq))
        (part 1#1#1 (use *)))
;∀N M.1≤K∧N'=M+K∧N≤M⊃1=K∧N=M